(set-logic QF_BV)
(declare-fun _substvar_16_ () (_ BitVec 1))
(declare-fun _substvar_23_ () (_ BitVec 1))
(declare-fun _substvar_70_ () Bool)
(declare-fun _substvar_15_ () (_ BitVec 32))
(declare-fun _substvar_14_ () (_ BitVec 32))
(declare-fun _substvar_69_ () Bool)
(declare-fun _substvar_20_ () (_ BitVec 1))
(declare-fun _substvar_25_ () (_ BitVec 1))
(declare-fun _substvar_24_ () (_ BitVec 1))
(declare-fun _substvar_17_ () (_ BitVec 1))
(assert (= false (bvult _substvar_15_ _substvar_14_)))
(assert (= _substvar_17_ _substvar_16_))
(assert (= _substvar_70_ _substvar_69_))
(assert (= _substvar_23_ _substvar_20_))
(assert (= (= _substvar_24_ (_ bv1 1)) (bvule _substvar_14_ _substvar_15_)))
(assert (= _substvar_25_ _substvar_24_))
(assert (= (_ bv0 1) (bvand _substvar_23_ _substvar_25_)))
(check-sat)
(exit)
